This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of an earlier paper and shows a strong normalization result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterization of normalizability of terms using intersection types.

This paper studies intersection and union type assignment for the calculus , a proof-term syntax for Gentzen’s classical sequent calculus, with the aim of defining a type-based semantics, via setting up a system that is closed under conversion. We will start by investigating what the minimal requirements are for a system, for to be complete ; this coincides with System , the notion defined in Dougherty et al. [18]; however, we show that this system is not sound , so our (...) goal cannot be achieved. We will then show that System is also not complete, but can recover from this by presenting System as an extension of and showing that it satisfies completeness; it still lacks soundness. We show how to restrict so that it satisfies soundness as well by limiting the applicability of certain type assignment rules, but only when limiting reduction to call-by-name or call-by-value reduction; in restricting the system this way, we sacrifice completeness. These results when combined show that, with respect to full reduction, it is not possible to define a sound and complete intersection and union type assignment system for. (shrink)

We study the cube of type assignment systems, as introduced in Giannini et al. 87–126), and confront it with Barendregt's typed gl-cube . The first is obtained from the latter through applying a natural type erasing function E to derivation rules, that erases type information from terms. In particular, we address the question whether a judgement, derivable in a type assignment system, is always an erasure of a derivable judgement in a corresponding typed system; we show that this property holds (...) only for systems without polymorphism. The type assignment systems we consider satisfy the properties ‘subject reduction’ and ‘strong normalization’. Moreover, we define a new type assignment cube that is isomorphic to the typed one. (shrink)